Inference at * 1 2 1 1 
Iof proof for Lemma integer sqrt:



1. n : 
2. 0 < n
3. r : 
4. (r * r)  (n - 1)
5. (n - 1) < ((r+1) * (r+1))
6. ((r+1) * (r+1))  n
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by With r+1 (D 0) THEN Auto' 

latex

 .

Definitions	n+m, #$n, x:A. B(x), A, False, P  Q, Void, -n, Type, n - m, P & Q, x:A  B(x), x:A. B(x), x:AB(x), s = t, A  B, S  T, |g|, , , {x:A| B(x)} , , a < b, n * m, t  T
Lemmas	nat wf, member wf, le wf